1. Field of the Invention
The present invention relates to verification and in particular to deriving invariants from constraints using binary decision diagrams (BDDs), wherein such invariants can advantageously reduce system resources during formal verification.
2. Related Art
To determine the correctness of a design or a module (hereinafter called a design) for an integrated circuit, a set of constraints is generally used. As used herein, a “constraint” describes a variable or a relationship between two or more variables. Sets of constraints can be used for both simulation and for formal verification of a design.
For example, by using constraint solving, the set of constraints can guide simulations to have only valid input values satisfying the constraints. In one known technique, totally random values can be assigned to the inputs of the design. By looking at the outputs of the design, invalid inputs can be identified and then eliminated from the set of constraints. For example, if outputs indicate that input A is always different than input B (i.e. A≠B), then the condition A=B can be eliminated from the set of constraints. This elimination process is called constrained random simulation. A binary decision diagram (BDD) is a data structure that can indicate the valid constraint combinations for a design. In one embodiment, a BDD can take the form of nested if-thens. In another embodiment, a BDD can take the form of a rooted, directed, acyclic graph that includes decision nodes (each decision node labeled by a Boolean variable) and two terminal nodes (0-terminal and 1-terminal). FIG. 1A illustrates an exemplary truth table 100. FIG. 1B illustrates a corresponding BDD 110 for the truth table 100. BDDs can be used during a subsequent simulation of the design.
In formal verification, constraints can be augmented with the design so that only valid transitions are considered in formal verification. Note that as used herein the term “formal verification” can include both logic design and functional verification as well as netlist verification. A “valid” transition means a transition from one state to another state by an input satisfying the constraints. Such transitions are typically associated with finite state machines (FSMs). In formal verification, all transitions of the design are considered at any point in time (which is called an implicit operation). That is, an individual transition of the design is not analyzed (which is called an explicit operation). In formal verification, any sets of invalid transitions are eliminated.
Notably, the design sizes that conventional formal verification can handle are small compared to those handled during simulation. For example, simulations can handle millions of registers, whereas formal verification typically only handles up to thousands of registers. Therefore, a need arises for a technique to more efficiently leverage constraint solving to improve the overall performance of formal verification.